did-forward(es; Sys; f; e) == a:E(Sys). (f(a) = e & ((loc(f(a)) = loc(a)))) 

latex

---

clarification:

did-forward(es; Sys; f; e)
== a:es-E-interface(es;Sys)
== (f(a) = e  es-E(es) & ((es-loc(es; (f(a))) = es-loc(es; a)  Id))) 

latex

Up	abstract chain replication
Wellformedness Lemmas	did-forward wf
Definitions	x:A. B(x), E(X), P & Q, E, A, s = t, Id, f(a), loc(e)
FDL editor aliases	did-forward